(declare-fun s0 () (_ FloatingPoint 8 24))
(declare-fun s1 () (_ FloatingPoint 8 24))
(declare-fun s14 () (_ BitVec 32))
(declare-fun s241 () (_ BitVec 32))
(assert s5)
(assert s6)
(assert s9)
(assert s16)
(assert (= s240 s241))
(check-sat)
